T:Type, L:(T List). iseg(T; L; [])  (null(L)) 

latex

Definitions	Y, append(as; bs), if b then t else f fi , tt, T, True, null(as), b, prop{i:l}, P  Q, P  Q, P  Q, x:A. B(x), P  Q, t  T, x:A. B(x), iseg(T; l1; l2), False, A, P  Q, decidable(P)
Lemmas	assert of null, btrue wf, append is nil, bool wf, true wf, squash wf, not wf, decidable assert, null wf, assert wf, append wf